no\_repeats($T$; $l$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$i$,$j$:$\mathbb{N}$. ($i$ $<$ $\parallel$$l$$\parallel$) $\Rightarrow$ ($j$ $<$ $\parallel$$l$$\parallel$) $\Rightarrow$ ($\neg$($i$ = $j$)) $\Rightarrow$ ($\neg$($l$[$i$] = $l$[$j$]))